\label{runningExample}

\subsection{Transformation Example}
Let us present the DSLTrans running example we will use throughout this paper. 

\begin{figure}[ht]
	\centering
		\includegraphics[scale=0.5]{images/squadagent.png}
		\includegraphics[scale=0.5]{images/squadsex.png}
	\caption{Metamodels of a squad of agents(left) and a squad organized by
	gender(right).}
	\label{squadmetamodel}
\end{figure}

\begin{figure}[h!]
	\centering
		\includegraphics[scale=0.45]{images/policesquad.pdf}
	\caption{A model transformation expressed in DSLTrans.}
	\label{dsltransformation}
\end{figure}

\begin{figure}[h]
	\centering
		\includegraphics[scale=0.12]{images/model_police_hierarchy.png}
		\includegraphics[scale=0.5]{images/model_police_gender.png}
	\caption{Original model (left) and transformed model (right).}
	\label{transformationexample}
\end{figure}

Figure~\ref{squadmetamodel} presents two metamodels of
languages for describing views over the organization of a police station. The metamodel annotated with
'Organization Language' represents a language for describing the chain of
command in a police station, which includes male ($Male$ class) and
female officers ($Female$ class). The metamodel annotated
with 'Gender Language' represents a language for describing a different view over
the chain of command, where the officers working at the police station are
classified by gender. In figure \ref{dsltransformation} we present a transformation written in DSLTrans\footnote{DSLTrans was deployed as an Eclipse plug-in~\cite{dsltransplugin}. The example shown in figure
\ref{dsltransformation}, was expressed using a concrete visual syntax of an Eclipse
diagrammatic editor.}
between models of both languages. The purpose of this transformation is to
flatten a chain of command given in language 'Organization Language' into two independent sets of male and female officers. Within each of those sets the command
relations are kept, i.e. a female officer will be directly related to all her
female subordinates and likewise for male officers. 


An example of an instance of this
transformation can be observed in figure \ref{transformationexample}, where the
original model is on the left and the transformed one on the right. Notice that
the elements $s$, $m_k$  and $f_k$ in the figure on the left are instances of
the source metamodel elements $Station$, $Male$ and $Female$ respectively (in
figure~\ref{squadmetamodel}). The primed elements in the figure on the right are
their instance counterparts in the target metamodel.

%\subsection{Layers}

A transformation in DSLTrans is formed by a set of input model
sources called \emph{file-ports} ('inputSquad.xmi' in figure
\ref{dsltransformation}) and a list of \emph{layers} ('Basic entities' and
'Relations' layers in figure \ref{dsltransformation}). Both layers and
file-ports are typed according to metamodels. DSLTrans executes sequentially the
list of layers of a transformation specification. A layer is a set of
transformation rules, which executes in a non-deterministic fashion. Each
transformation rule is a pair $(match,apply)$ where $match$ is a pattern
holding elements from the source metamodel, and $apply$ is a pattern holding elements of
the target metamodel. For example, in the transformation rule 'Stations' in the
'Basic entities' layer (in figure \ref{dsltransformation}) the $match$ pattern
holds one 'Station' class from the 'Squad Organization Language' metamodel ---
the source metamodel; the $apply$ pattern holds one 'Station' class from the
'Squad Gender Language' metamodel --- the target metamodel. This means that all
elements in the input source which are of type 'Station' of the source metamodel
will be transformed into elements of type 'Station' of the target metamodel. 

Let us first define the constructs available for building transformation rules'
match patterns. We will illustrate the constructs by referring to the transformation in figure~\ref{dsltransformation}.

\begin{itemize}
\item \emph{Match Elements}: are variables typed by elements of the source
metamodel which can assume as values elements of that type (or subtype) in the
input model. In our example, a match element is the 'Station' element in the
'Stations' transformation rule of layer 'Basic Entities' layer;

\item \emph{Attribute Conditions}: conditions over the attributes of a $match$ element;

\item \emph{Direct Match Links}:  are variables typed by labelled relations of
the source metamodel. These variables can assume as values relations having the
same label in the input model. A direct match link is always expressed between two match elements;

\item \emph{Indirect Match Links}: indirect match links are similar to direct match
links, but there may exist a path of containment associations between the
matched instances\footnote{In the implementation the notion of indirect links
only captures EMF containment associations in order to avoid cycles.}. In our
example, indirect match links are represented in all the transformation rules of
layer 'Relations' as dashed arrows between elements of the match models;

\item \emph{Backward Links}: backward links connect elements of the match and the
apply models. They exist in our example in all transformation rules in the
'Relations' layer, depicted as dashed vertical lines. Backward links are used to
refer to elements created in a previous layer in order to use them in the
current one. An important characteristic of DSLTrans is that
throughout all the layers the source model remains intact as a match source. Therefore, the only
possibility to reuse elements created from a previous layer is to reference them
using backward links;

\item \emph{Negative Conditions}: it is possible to express negative conditions over
match elements, backward, direct and indirect match links. 
\end{itemize}

The constructs for building transformation rules' apply patterns are:

\begin{itemize}
\item \emph{Apply Elements and Apply Links}: apply elements, as match elements,
are variables typed by elements of the source metamodel. Apply elements in a
given transformation rule that are not connected to backward links will create
elements of the same type in the transformation output. A similar mechanism is
used for apply links. These output elements and links will be created as many
times as the match model of the transformation rule is instantiated in the input
model. In our example, the 'StationwMale' transformation rule of layer
'Relations Layer' takes instances of $Station$ and $Male$ (of the 'Gender
Language' metamodel) which were created in a previous layer from instances of
$Station$ and $Male$ (of the 'Organization Language' metamodel), and connects
them using a 'male' relation;

\item \emph{Apply Attributes}: DSLTrans includes a small attribute language
allowing the composition of attributes of apply model elements from references
to one or more match model element attributes.
\end{itemize}

\subsection{Verification Example}

\begin{figure}[ht]
	\centering
		\includegraphics[scale=0.55]{images/policesquadproperties.png}
	\caption{Validation properties over a DSLTrans model.}
	\label{dlstransproperty}
\end{figure}

\begin{figure}[ht]
	\centering
		\includegraphics[scale=0.23]{images/state_space.png}
	\caption{Partial state space for the transformation in Fig.~\ref{dlstransformation}.}
	\label{statespace}
\end{figure}

Now that the transformation language has been defined we can move on to describe
the properties we wish to prove about our transformations. Examples of these properties can
be observed in Fig.~\ref{dlstransproperty}. In natural language the property
named `Satisfiable Property' reads as follows: `Any model which includes a police
station that has both a male and female chief officers will be transformed into
a model where the male chief officer will exist in the male set and the female
chief officer will exist in the female set'. The primary goal of our model
checker is to prove that, given a transformation, such a property will hold
for all models given as inputs to that transformation.

%(##) starts with the initial state
Practically, this proof is achieved by building what we call the state space of a
transformation. Each state of the transformation state space corresponds to a
possible combination of the transformation rules of a given layer, combined with all
states of the previous layer. Using the example of the transformation given in
Fig.~\ref{dlstransformation} we can build a rough sketch of such a state space
which we present in Fig.\ref{statespace}. In the figure we identify each
transformation rule in each layer by a number with an index. For example
transformation $1_1$ corresponds to the first transformation --- e.g. left to
right in Fig.~\ref{dlstransformation} --- in layer one. The state space
starts with the initial state--- which in the figure belongs to layer 0 ---
where no transformation has been applied.  The initial state then connects to
all possibilities of combinations of transformation rules in layer 1. Each of
the states produced by layer 1 is then connected to all possibilities of
combinations of transformation rules in layer 2 --- in the figure we only
exemplify with the state $3_1$. The states in layer 2 include not only the
combinations of transformation rules from that layer, but also the
transformation rules coming from a state produced by the previous layer. In
such a way each state accumulates all transformation rules leading to it and
thus a describes pattern(s) that should exist in the source model. As such,
each state symbolically describes an equivalence class of input models.

\begin{figure}[ht]
	\centering
		\includegraphics[scale=0.5]{images/premerge.png}
		\includegraphics[scale=0.5]{images/merge.png}
	\caption{Original transformations rules (left) and a possible collapse of those rules (right).}
	\label{transformationmergeexample}
\end{figure}

We can be more precise while building such equivalence classes. In
Fig.~\ref{transformationmergeexample} we exemplify what we call the
\emph{collapse} of two of the rules of the transformation in
Fig.~\ref{dlstransformation}. Due to the semantics of DSLTrans it may occur
that, for example, if we have the two transformations on the left of
Fig.~\ref{transformationmergeexample} applied to a model, the instance of
$Station$ used by the match pattern of the two rules is the same. This comes from
the fact that, in DSLTrans, the same input can consumed by several transformation
rules within the same layer. In this case we can collapse the two classes in one
in the state we are building. In fact, we can even go further and collapse the
$Station$ classes in the apply pattern of the two rules which would mean that
both $Station$ instances previously created in layer 1 (notice the backward link)
are actually the same. This leads to the state shown in
Fig.~\ref{transformationmergeexample} on the right. In fact this state is
required to prove the `Satisfiable Property' in Fig.~\ref{dlstransproperty}.

%(##) removed the more in 'becomes more complete'
More generally, \emph{collapsing} transformation rules is used to add more
definition to the equivalence classes represented by each state than the simple
union of transformations as can be seen in Fig.~\ref{dlstransformation}. In
this union, all elements of the same type in the disjoint graphs of the united
transformation are seen as referring to different objects in the input model
--- i.e. several elements of the same type within a transformation necessarily
refer to different objects in a model. By adding the collapsed transformation
rule states to the state space, the proofs of our properties become 
complete given we are covering more models in our symbolic states.\\

The proof of a property is then achieved by walking through the state space and
checking every complete transformation state space path (starting from the
initial state): if there is a state that satisfies the $match$ pattern of
the property, then there must exist a subsequent state for which the $apply$
pattern satisfies the $apply$ pattern of the property.

In Fig.\ref{dlstransproperty}, the property named `Unsatisfiable Property'
represents a property that is not true for the transformation in
Fig.~\ref{dlstransformation}. In natural language the property states the
following: `If a male officer commands a female officer in the original model,
then that relation will be preserved in the transformed mode'. In our simple
example, this is clearly not true given that the point of our transformation is
to build separate lists of male and female officers. That said, in order to be
proved, the property should hold on all paths of the state space, therefore it
is sufficient to find one path where the property does not hold to render the
property false. Such a path can then be used as a counterexample and may be
useful for the transformation designer in the sense that it may point out a
sequence of transformation rules leading to a wrong transformation result.

It may also happen that a property is non provable. In
Fig.~\ref{dlstransproperty}, the property named `Non Provable' refers to
dogs in the $match$ pattern, a situation which is never contemplated by the
transformation rules in Fig.~\ref{dlstransformation}. As such, the only
possible statement about this property is that, although the source metamodel
would allow such $match$ patterns, the transformation does not implement them.
This situation may point out to the transformation designer that (s)he is
missing transformation rules to address certain patterns of the input models.
